Properly track safety invariants #1237
Conversation
Manishearth
force-pushed
the
safety-invariants
branch
from
37f7472 to
6587eea
Compare
This means only the code in tree.rs has the ability to violate the relevant invariants
There was a problem hiding this comment.
Thanks so much for showing how it's done, so much better than what was there before!
This also sets the bar for unsafe in this project, and I will look back here when documenting the next (or an existing) unsafe part of the project, in the hopes to uphold this standard by enforcing invariants on fields and documenting them.
| /// was constructed using that Tree's child_items. This works since Tree has this invariant as well: all | ||
| /// child_items are referenced at most once (really, exactly once) by a node in the tree. | ||
| #[allow(clippy::too_many_arguments, unsafe_code)] | ||
| #[deny(unsafe_op_in_unsafe_fn)] // this is a big function, require unsafe for the one small unsafe op we have |
There was a problem hiding this comment.
That is great!! I wasn't aware of this effective means of propagating unsafe the way it should be propagated without making it incredibly easy to embed even more unsafe calls or expressed differently, make the unsafe-review-surface even larger.
| #[allow(unsafe_code)] | ||
| unsafe impl<T> Send for ItemSliceSync<'_, T> where T: Send {} | ||
| // SAFETY: T is `Send`, and as long as the user follows the contract of | ||
| // `get_mut()`, we only ever access one T at a time. | ||
| // SAFETY: This is logically an &mut T, which is Sync if T is Sync |
There was a problem hiding this comment.
This I never really understood as my intuition was that the bound should be Sync if T: Sync for perfect safety. But having to say it's Sync if T: Send seems to be too broad and also allows RefCells for instance which are !Sync.
Is this a shortcoming of the type system, or a shortcoming of the way ItemSliceSync is defined, or something entirely different (like me not understanding how Send + Sync truly works beyond some intuition from practice :D).
Helps with #1231
Would be ideal to have an architecture where this isn't necessary, but this properly documents every field that has an invariant and how that invariant is upheld in every place it is changed.
In general for safety invariants whilst having whole-program explanations of safety are useful, they rely on the entire program behaving the way you expect it, which is not easy to verify in complex code. It is preferable to document every invariant and justify that it is upheld in every position where there is potential for it to break, so that the invariants can be traced through. It is ideal to structure the unsafe such that there are limited places for this to be necessary.